Attributed C-sets in CatColab

Several levels in CatColab

• double theories, which are double categories, possibly with extra structure
  • called "logic" in the tool
• A theory has models
  • the main thing that you are editing in the tool
  • a model is a structure-preserving lax functor from the theory into the double category called \(\mathbb{Set}\) or \(\mathbb{Span}\)
• A model can have instances
  • not implemented yet
  • in ACSets.jl: they are in the form of interlinked columnar tables
  • model vs. instances:
    • models are categorical structures, consists of objects and morphisms, possibly with functorial operations acting on them
    • instances are set-theoretical structures, consists of elements, possibly with functional operations acting on them

Here are a few examples. The "trivial," but important and motivating, example is when the double theory is the point (the terminal double category). Then a model is a category, say \(\mathsf{C}\), and an instance of that model is a copresheaf on \(\mathsf{C}\), i.e., a functor \(\mathsf{C} \to \mathsf{Set}\). So that how \(\mathsf{C}\)-sets fit in. There is a double theory whose models are multicategories, i.e., typed operads. An instance is then a functor into the multicategory of sets and functions of several variables, i.e., an algebra of the operad.

• related:
  • theory, model
  • mentioned: acset